A. Chagrov, M. Zakharyaschev; "Modal Logic", Prop 1.8
Prop
有限タブロー$ t_1が充足可能$ \iff
何らかのタブロー列$ t_1,\dots,t_nが構成できて,以下を満たす.
$ t_nは非交和飽和
$ t_{i+1}は$ t_iに充足規則を適用したもの.
Memo
おそらく,タブロー列が非交和飽和であることが肝心であるとすると充足規則が教科書のものである必要はなく,次のように改変しても良いと思われる.
タブロー$ t_i = (\Gamma_i,\Delta_i)に対して,高々2つのタブロー$ t^1_{i+1},t^2_{i+1}を生成する規則SA1' ~ SA6'を次のように定める.
SA1': $ \psi \land \xi \in \Gamma_iとなる$ \psi \land \xiが存在するとき,$ t^1_{i+1} = (\Gamma_i \cup \{\psi,\xi\} \setminus \{\psi \land \xi\},\Delta)する.($ t^2_{i+1}は無い)
SA2': $ \psi \land \xi \in \Delta_iとなる$ \psi \land \xiが存在するとき,↓とする.
$ t^1_{i+1} = (\Gamma_i,\Delta_i \cup \{\psi\} \setminus \{\psi \land \xi\})
$ t^2_{i+1} = (\Gamma_i,\Delta_i \cup \{\xi\} \setminus \{\psi \land \xi\})
SA3' ~ SA6'も同様に定める.
今,各々のパーツの重さを次のように定める
論理式$ \varphi:$ \mathrm{wgt}(\varphi)を$ \varphiの$ \botを除いた論理記号の数
論理式の集合$ \Gamma:$ \mathrm{wgt}(\Gamma) := \sum_{\varphi \in \Gamma} \mathrm{wgt}(\varphi)を
タブロー$ t:$ \mathrm{wgt}(t) = \mathrm{wgt}(\Gamma) + \mathrm{wgt}(\Delta)
さて明らかに次のことが成り立つ.
タブローは有限だからその重さも有限である.
論理式の構造から考えて,タブローの重さが0であることは,タブローの$ \Gamma,\Delta \sube \mathrm{Var}であることを意味する
$ \Gamma,\Delta = \emptyもあることに注意
タブロー$ t_iに適当に規則を適用してできたタブロー$ t^j_{i+1}の重さはかならず元のタブローの重さより減る.
すなわち$ \mathrm{wgt}(t_i) > \mathrm{wgt}(t^j_{i+1})である.
$ \mathrm{wgt}(t_i) \ge 1であるということは$ t_iに規則を適用可能な論理式がまだ残っているということである.
これらを踏まえると,任意のタブローは重さが0になるまで有限回で規則を適用し続けることが可能であり,限界で命題変項だけを含んだタブローが得られる.
いくつかの規則でタブローは分岐するが,分岐は高々2個であることと先程の事実を踏まえると,命題変項だけを含んだタブローに辿り着いても高々有限回分岐して有限個のタブロー列が得られるだけである.
具体的には$ 2^{|\mathrm{Sub}(\Gamma)| + |\mathrm{Sub}(\Delta)|}で抑えられるはず
当然SA1' ~ SA6'は非交和性と飽和性を維持しながらタブローを小さくしていくので,最後の